Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(max,0),x)  → x
2:    app(app(max,x),0)  → x
3:    app(app(max,app(s,x)),app(s,y))  → app(app(max,x),y)
4:    app(app(min,0),x)  → 0
5:    app(app(min,x),0)  → 0
6:    app(app(min,app(s,x)),app(s,y))  → app(app(min,x),y)
7:    app(app(app(app(insert,f),g),nil),x)  → app(app(cons,x),nil)
8:    app(app(app(app(insert,f),g),app(app(cons,h),t)),x)  → app(app(cons,app(app(f,x),h)),app(app(app(app(insert,f),g),t),app(app(g,x),h)))
9:    app(app(app(sort,f),g),nil)  → nil
10:    app(app(app(sort,f),g),app(app(cons,h),t))  → app(app(app(app(insert,f),g),app(app(app(sort,f),g),t)),h)
11:    app(ascending_sort,l)  → app(app(app(sort,min),max),l)
12:    app(descending_sort,l)  → app(app(app(sort,max),min),l)
There are 25 dependency pairs:
13:    APP(app(max,app(s,x)),app(s,y))  → APP(app(max,x),y)
14:    APP(app(max,app(s,x)),app(s,y))  → APP(max,x)
15:    APP(app(min,app(s,x)),app(s,y))  → APP(app(min,x),y)
16:    APP(app(min,app(s,x)),app(s,y))  → APP(min,x)
17:    APP(app(app(app(insert,f),g),nil),x)  → APP(app(cons,x),nil)
18:    APP(app(app(app(insert,f),g),nil),x)  → APP(cons,x)
19:    APP(app(app(app(insert,f),g),app(app(cons,h),t)),x)  → APP(app(cons,app(app(f,x),h)),app(app(app(app(insert,f),g),t),app(app(g,x),h)))
20:    APP(app(app(app(insert,f),g),app(app(cons,h),t)),x)  → APP(cons,app(app(f,x),h))
21:    APP(app(app(app(insert,f),g),app(app(cons,h),t)),x)  → APP(app(f,x),h)
22:    APP(app(app(app(insert,f),g),app(app(cons,h),t)),x)  → APP(f,x)
23:    APP(app(app(app(insert,f),g),app(app(cons,h),t)),x)  → APP(app(app(app(insert,f),g),t),app(app(g,x),h))
24:    APP(app(app(app(insert,f),g),app(app(cons,h),t)),x)  → APP(app(app(insert,f),g),t)
25:    APP(app(app(app(insert,f),g),app(app(cons,h),t)),x)  → APP(app(g,x),h)
26:    APP(app(app(app(insert,f),g),app(app(cons,h),t)),x)  → APP(g,x)
27:    APP(app(app(sort,f),g),app(app(cons,h),t))  → APP(app(app(app(insert,f),g),app(app(app(sort,f),g),t)),h)
28:    APP(app(app(sort,f),g),app(app(cons,h),t))  → APP(app(app(insert,f),g),app(app(app(sort,f),g),t))
29:    APP(app(app(sort,f),g),app(app(cons,h),t))  → APP(app(insert,f),g)
30:    APP(app(app(sort,f),g),app(app(cons,h),t))  → APP(insert,f)
31:    APP(app(app(sort,f),g),app(app(cons,h),t))  → APP(app(app(sort,f),g),t)
32:    APP(ascending_sort,l)  → APP(app(app(sort,min),max),l)
33:    APP(ascending_sort,l)  → APP(app(sort,min),max)
34:    APP(ascending_sort,l)  → APP(sort,min)
35:    APP(descending_sort,l)  → APP(app(app(sort,max),min),l)
36:    APP(descending_sort,l)  → APP(app(sort,max),min)
37:    APP(descending_sort,l)  → APP(sort,max)
The approximated dependency graph contains one SCC: {13,15,17,19,21-29,31-33,35,36}.
Tyrolean Termination Tool  (112.47 seconds)   ---  May 3, 2006